;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
; Interface for the photonegative module, 
; which takes in an image and produces its
; inverted photo.
(interface IPhotonegative
  
  (sig photonegative (tree))
  (sig photonegative-helper (oldtree newtree xcurr xmax ycurr ymax))
  
  ; verifies that photonegative returns a tree structure
  (con photonegative-returns-tree
       (implies (tree? tr))
       (tree? (photonegative tr)))
  
  ; verifies that photonegative-helper returns a tree
  (con photonegative-helper-returns-tree
       (implies (and (tree? oldtr) (tree? newtr) (= xcurr 0) 
                     (= ycurr 0) (natp xmax) (natp ymax)))
       (tree? (photonegative-helper oldtr newtr xcurr xmax ycurr ymax))))